Fixpoint add n m :=
  match n with
  | 0 => m
  | S p => S (p + m)
  end

where "n + m " := (add n m) : nat_scope.

Lemma n_plus_zero_equals_n:
  forall n, (add n O) = n.
Proof.
  induction n.
  - reflexivity.
  - simpl. rewrite IHn. reflexivity.
Qed.